perm filename DLO.ERL[1,JRA] blob
sn#005864 filedate 1972-07-24 generic text, type T, neo UTF8
00100 LE(X1 X2) ∨ LE(X2 X1);
00200 (LE(X1 X2) ∧ LE(X2 X1))→ E(X1 X2);
00300 (LE(X1 X2) ∧ LE(X2 X3)) → LE(X1 X3);
00400 LE(X1 ADD1(X1));
00500 ¬E(X1 ADD1(X1));
00600 LE(X2 X1) ∨ LE(ADD1(X1) X2);
00700 LE(X1 X1);
00800 ;
00900 ;
00100
00200 ∀(X1 X2 X3 X4)((((LE(ADD1(X2) X1) ∧ LE(X1 X3))→LE(A(X1) A(ADD1(X1)))) ∧( LE(X2 X3) →LE(A(X2) A(ADD1(X2)))))
00300 → ((LE(X2 X4) ∧ LE(X4 X3) )→ LE(A(X4) A(ADD1(X4)))));
00400 ;
00500